T:Type, P:(T), f:(x:T. Dec(P(x))), x:T.
(can-apply(p-co-filter(f);x))  (do-apply(p-co-filter(f);x) = x) 

latex

ProofTree

Definitions

b, do-apply(f;x), p-co-filter(f), can-apply(f;x), x:AB(x), s = t, P  Q, x:A. B(x), f(a), x(s), Dec(P), Type, , True, False, left + right, P  Q, t  T